On sufficient-completeness and related properties of term rewriting systems
Identifieur interne : 00E607 ( Main/Exploration ); précédent : 00E606; suivant : 00E608On sufficient-completeness and related properties of term rewriting systems
Auteurs : Deepak Kapur [États-Unis] ; Paliath Narendran [États-Unis] ; Hantao Zhang [États-Unis]Source :
- Acta Informatica [ 0001-5903 ] ; 1987-08-01.
English descriptors
- Teeft :
- Abstract data types, Complete term, Confluent, Data type, Decidability, Decidable, Distinct positions, Distinct terms, Distinct tuples, Equational, Equational specification, Equational specifications, Function symbol, Function symbols, Global reduction, Ground instance, Ground substitution, Ground term, Ground terms, Inductive properties, Irreducible, Irreducible ground term, Irreducible ground terms, Kapur, Kounalis, Main theorem, Nonconstructor, Normal form, Other words, Range type, Reducible, Specification, Substitution, Subterm, Sufficient completeness, Thue, Thue system, Thue systems, Transitive closure, Type hierarchy, Type names, Undecidable.
Abstract
Summary: The decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.
Url:
DOI: 10.1007/BF00292110
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001409
- to stream Istex, to step Curation: 001392
- to stream Istex, to step Checkpoint: 003536
- to stream Main, to step Merge: 00EE94
- to stream Main, to step Curation: 00E607
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">On sufficient-completeness and related properties of term rewriting systems</title><author><name sortKey="Kapur, Deepak" sort="Kapur, Deepak" uniqKey="Kapur D" first="Deepak" last="Kapur">Deepak Kapur</name></author><author><name sortKey="Narendran, Paliath" sort="Narendran, Paliath" uniqKey="Narendran P" first="Paliath" last="Narendran">Paliath Narendran</name></author><author><name sortKey="Zhang, Hantao" sort="Zhang, Hantao" uniqKey="Zhang H" first="Hantao" last="Zhang">Hantao Zhang</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:55BDC74D8473B32386B1322DFED31CD8B71B6988</idno><date when="1987" year="1987">1987</date><idno type="doi">10.1007/BF00292110</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-MVDCBV5H-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001409</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001409</idno><idno type="wicri:Area/Istex/Curation">001392</idno><idno type="wicri:Area/Istex/Checkpoint">003536</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003536</idno><idno type="wicri:doubleKey">0001-5903:1987:Kapur D:on:sufficient:completeness</idno><idno type="wicri:Area/Main/Merge">00EE94</idno><idno type="wicri:Area/Main/Curation">00E607</idno><idno type="wicri:Area/Main/Exploration">00E607</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">On sufficient-completeness and related properties of term rewriting systems</title><author><name sortKey="Kapur, Deepak" sort="Kapur, Deepak" uniqKey="Kapur D" first="Deepak" last="Kapur">Deepak Kapur</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Corporate Research and Development, General Electric Company, 12345, Schenectady, NY</wicri:regionArea><placeName><region type="state">État de New York</region></placeName></affiliation></author><author><name sortKey="Narendran, Paliath" sort="Narendran, Paliath" uniqKey="Narendran P" first="Paliath" last="Narendran">Paliath Narendran</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Corporate Research and Development, General Electric Company, 12345, Schenectady, NY</wicri:regionArea><placeName><region type="state">État de New York</region></placeName></affiliation></author><author><name sortKey="Zhang, Hantao" sort="Zhang, Hantao" uniqKey="Zhang H" first="Hantao" last="Zhang">Hantao Zhang</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>Department of Computer Science, Rensselaer Polytechnic Institute, 12181, Troy, NY</wicri:regionArea><placeName><region type="state">État de New York</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Acta Informatica</title><title level="j" type="abbrev">Acta Informatica</title><idno type="ISSN">0001-5903</idno><idno type="eISSN">1432-0525</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1987-08-01">1987-08-01</date><biblScope unit="volume">24</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="395">395</biblScope><biblScope unit="page" to="415">415</biblScope></imprint><idno type="ISSN">0001-5903</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0001-5903</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract data types</term><term>Complete term</term><term>Confluent</term><term>Data type</term><term>Decidability</term><term>Decidable</term><term>Distinct positions</term><term>Distinct terms</term><term>Distinct tuples</term><term>Equational</term><term>Equational specification</term><term>Equational specifications</term><term>Function symbol</term><term>Function symbols</term><term>Global reduction</term><term>Ground instance</term><term>Ground substitution</term><term>Ground term</term><term>Ground terms</term><term>Inductive properties</term><term>Irreducible</term><term>Irreducible ground term</term><term>Irreducible ground terms</term><term>Kapur</term><term>Kounalis</term><term>Main theorem</term><term>Nonconstructor</term><term>Normal form</term><term>Other words</term><term>Range type</term><term>Reducible</term><term>Specification</term><term>Substitution</term><term>Subterm</term><term>Sufficient completeness</term><term>Thue</term><term>Thue system</term><term>Thue systems</term><term>Transitive closure</term><term>Type hierarchy</term><term>Type names</term><term>Undecidable</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Summary: The decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>État de New York</li></region></list><tree><country name="États-Unis"><region name="État de New York"><name sortKey="Kapur, Deepak" sort="Kapur, Deepak" uniqKey="Kapur D" first="Deepak" last="Kapur">Deepak Kapur</name></region><name sortKey="Narendran, Paliath" sort="Narendran, Paliath" uniqKey="Narendran P" first="Paliath" last="Narendran">Paliath Narendran</name><name sortKey="Zhang, Hantao" sort="Zhang, Hantao" uniqKey="Zhang H" first="Hantao" last="Zhang">Hantao Zhang</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00E607 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00E607 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:55BDC74D8473B32386B1322DFED31CD8B71B6988
|texte= On sufficient-completeness and related properties of term rewriting systems
}}
| This area was generated with Dilib version V0.6.33. |  |